Left Termination proof of /tmp/tmpr1P6w5/pl8.2.1.pl

Left Termination of the query pattern mergesort_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

mergesort([], []).
mergesort(.(E, []), .(E, [])).
mergesort(.(E, .(F, U)), V) :- ','(split(.(E, .(F, U)), W, Y), ','(mergesort(W, X), ','(mergesort(Y, Z), merge(X, Z, V)))).
merge(X, [], X).
merge([], X, X).
merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z)).
merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z)).
split([], [], []).
split(.(E, U), .(E, V), W) :- split(U, W, V).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Queries:

mergesort(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

MERGESORT_IN(.(E, .(F, U)), V) → U1¹(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
MERGESORT_IN(.(E, .(F, U)), V) → SPLIT_IN(.(E, .(F, U)), W, Y)
SPLIT_IN(.(E, U), .(E, V), W) → U9¹(E, U, V, W, split_in(U, W, V))
SPLIT_IN(.(E, U), .(E, V), W) → SPLIT_IN(U, W, V)
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2¹(E, F, U, V, Y, mergesort_in(W, X))
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → MERGESORT_IN(W, X)
U2¹(E, F, U, V, Y, mergesort_out(W, X)) → U3¹(E, F, U, V, X, mergesort_in(Y, Z))
U2¹(E, F, U, V, Y, mergesort_out(W, X)) → MERGESORT_IN(Y, Z)
U3¹(E, F, U, V, X, mergesort_out(Y, Z)) → U4¹(E, F, U, V, merge_in(X, Z, V))
U3¹(E, F, U, V, X, mergesort_out(Y, Z)) → MERGE_IN(X, Z, V)
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U7¹(A, X, B, Y, Z, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → GT_IN(A, B)
GT_IN(s(X), s(Y)) → U10¹(X, Y, gt_in(X, Y))
GT_IN(s(X), s(Y)) → GT_IN(X, Y)
U7¹(A, X, B, Y, Z, gt_out(A, B)) → U8¹(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
U7¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U5¹(A, X, B, Y, Z, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → LE_IN(A, B)
LE_IN(s(X), s(Y)) → U11¹(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U5¹(A, X, B, Y, Z, le_out(A, B)) → U6¹(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
U5¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

The argument filtering Pi contains the following mapping:
mergesort_in(x1, x2) = mergesort_in(x1)
.(x1, x2) = .(x1, x2)
U1(x1, x2, x3, x4, x5) = U1(x5)
split_in(x1, x2, x3) = split_in(x1)
U9(x1, x2, x3, x4, x5) = U9(x1, x5)
[] = []
split_out(x1, x2, x3) = split_out(x2, x3)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
mergesort_out(x1, x2) = mergesort_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x5, x6)
U4(x1, x2, x3, x4, x5) = U4(x5)
merge_in(x1, x2, x3) = merge_in(x1, x2)
U7(x1, x2, x3, x4, x5, x6) = U7(x1, x2, x3, x4, x6)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
0 = 0
gt_out(x1, x2) = gt_out
U10(x1, x2, x3) = U10(x3)
U8(x1, x2, x3, x4, x5, x6) = U8(x3, x6)
U5(x1, x2, x3, x4, x5, x6) = U5(x1, x2, x3, x4, x6)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U11(x1, x2, x3) = U11(x3)
U6(x1, x2, x3, x4, x5, x6) = U6(x1, x6)
merge_out(x1, x2, x3) = merge_out(x3)
U11¹(x1, x2, x3) = U11¹(x3)
SPLIT_IN(x1, x2, x3) = SPLIT_IN(x1)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U5¹(x1, x2, x3, x4, x5, x6) = U5¹(x1, x2, x3, x4, x6)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x5, x6)
U9¹(x1, x2, x3, x4, x5) = U9¹(x1, x5)
U8¹(x1, x2, x3, x4, x5, x6) = U8¹(x3, x6)
LE_IN(x1, x2) = LE_IN(x1, x2)
U1¹(x1, x2, x3, x4, x5) = U1¹(x5)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x5, x6)
U7¹(x1, x2, x3, x4, x5, x6) = U7¹(x1, x2, x3, x4, x6)
U10¹(x1, x2, x3) = U10¹(x3)
U4¹(x1, x2, x3, x4, x5) = U4¹(x5)
GT_IN(x1, x2) = GT_IN(x1, x2)
U6¹(x1, x2, x3, x4, x5, x6) = U6¹(x1, x6)
MERGESORT_IN(x1, x2) = MERGESORT_IN(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

MERGESORT_IN(.(E, .(F, U)), V) → U1¹(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
MERGESORT_IN(.(E, .(F, U)), V) → SPLIT_IN(.(E, .(F, U)), W, Y)
SPLIT_IN(.(E, U), .(E, V), W) → U9¹(E, U, V, W, split_in(U, W, V))
SPLIT_IN(.(E, U), .(E, V), W) → SPLIT_IN(U, W, V)
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2¹(E, F, U, V, Y, mergesort_in(W, X))
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → MERGESORT_IN(W, X)
U2¹(E, F, U, V, Y, mergesort_out(W, X)) → U3¹(E, F, U, V, X, mergesort_in(Y, Z))
U2¹(E, F, U, V, Y, mergesort_out(W, X)) → MERGESORT_IN(Y, Z)
U3¹(E, F, U, V, X, mergesort_out(Y, Z)) → U4¹(E, F, U, V, merge_in(X, Z, V))
U3¹(E, F, U, V, X, mergesort_out(Y, Z)) → MERGE_IN(X, Z, V)
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U7¹(A, X, B, Y, Z, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → GT_IN(A, B)
GT_IN(s(X), s(Y)) → U10¹(X, Y, gt_in(X, Y))
GT_IN(s(X), s(Y)) → GT_IN(X, Y)
U7¹(A, X, B, Y, Z, gt_out(A, B)) → U8¹(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
U7¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U5¹(A, X, B, Y, Z, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → LE_IN(A, B)
LE_IN(s(X), s(Y)) → U11¹(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U5¹(A, X, B, Y, Z, le_out(A, B)) → U6¹(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
U5¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

From the DPs we obtained the following set of size-change graphs:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U7¹(A, X, B, Y, Z, gt_in(A, B))
U7¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U5¹(A, X, B, Y, Z, le_in(A, B))
U5¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

The argument filtering Pi contains the following mapping:
mergesort_in(x1, x2) = mergesort_in(x1)
.(x1, x2) = .(x1, x2)
U1(x1, x2, x3, x4, x5) = U1(x5)
split_in(x1, x2, x3) = split_in(x1)
U9(x1, x2, x3, x4, x5) = U9(x1, x5)
[] = []
split_out(x1, x2, x3) = split_out(x2, x3)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
mergesort_out(x1, x2) = mergesort_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x5, x6)
U4(x1, x2, x3, x4, x5) = U4(x5)
merge_in(x1, x2, x3) = merge_in(x1, x2)
U7(x1, x2, x3, x4, x5, x6) = U7(x1, x2, x3, x4, x6)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
0 = 0
gt_out(x1, x2) = gt_out
U10(x1, x2, x3) = U10(x3)
U8(x1, x2, x3, x4, x5, x6) = U8(x3, x6)
U5(x1, x2, x3, x4, x5, x6) = U5(x1, x2, x3, x4, x6)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U11(x1, x2, x3) = U11(x3)
U6(x1, x2, x3, x4, x5, x6) = U6(x1, x6)
merge_out(x1, x2, x3) = merge_out(x3)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U5¹(x1, x2, x3, x4, x5, x6) = U5¹(x1, x2, x3, x4, x6)
U7¹(x1, x2, x3, x4, x5, x6) = U7¹(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U7¹(A, X, B, Y, Z, gt_in(A, B))
U7¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U5¹(A, X, B, Y, Z, le_in(A, B))
U5¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
0 = 0
gt_out(x1, x2) = gt_out
U10(x1, x2, x3) = U10(x3)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U11(x1, x2, x3) = U11(x3)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U5¹(x1, x2, x3, x4, x5, x6) = U5¹(x1, x2, x3, x4, x6)
U7¹(x1, x2, x3, x4, x5, x6) = U7¹(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))
U7¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U10(gt_out) → gt_out
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U7¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The remaining pairs can at least be oriented weakly.

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))

Used ordering: Combined order from the following AFS and order.
MERGE_IN(x1, x2) = x2
.(x1, x2) = .(x1, x2)
U7¹(x1, x2, x3, x4, x5) = U7¹(x4, x5)
gt_in(x1, x2) = gt_in
U5¹(x1, x2, x3, x4, x5) = U5¹(x3, x4)
le_out = le_out
le_in(x1, x2) = le_in(x1, x2)
gt_out = gt_out
s(x1) = s
U10(x1) = x1
0 = 0
U11(x1) = x1

Recursive path order with status [2].
Quasi-Precedence:

s > [gt_in, gt_out]
0 > [.₂, U7^1₂, U5^1₂, le_out, le_{in_2]} > [gt_in, gt_out]

Status:

le_out: multiset
0: multiset
U5^1₂: [1,2]
s: []
.₂: [1,2]
gt_in: multiset
le_in₂: [1,2]
U7^1₂: [2,1]
gt_out: multiset

The following usable rules [17] were oriented:

gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
gt_in(s(X), 0) → gt_out

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U10(gt_out) → gt_out
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U10(gt_out) → gt_out
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

gt_in(x0, x1)
U10(x0)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ QDPSizeChangeProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out

The set Q consists of the following terms:

le_in(x0, x1)
U11(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
The graph contains the following edges 2 >= 1

We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))

The remaining pairs can at least be oriented weakly.

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))
U7¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

Used ordering: Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₁ + x₂
POL(0) = 0
POL(MERGE_IN(x₁, x₂)) = x₁
POL(U10(x₁)) = 0
POL(U11(x₁)) = 0
POL(U5¹(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂
POL(U7¹(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₂
POL(gt_in(x₁, x₂)) = 0
POL(gt_out) = 0
POL(le_in(x₁, x₂)) = 0
POL(le_out) = 0
POL(s(x₁)) = 0

The following usable rules [17] were oriented: none

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                          ↳ QDP

                        ↳ QDPOrderProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))
U7¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U10(gt_out) → gt_out
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MERGE_IN(.(A, X), .(B, Y)) → U5¹(A, X, B, Y, le_in(A, B))
U7¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The remaining pairs can at least be oriented weakly.

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( le_out ) =

/	1	\
\	1	/

M( U10(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	1	/

x₁

M( s(x₁) ) =

/	0	\
\	0	/

/	1	1	\
\	1	1	/

x₁

M( 0 ) =

/	1	\
\	0	/

M( U11(x₁) ) =

/	0	\
\	0	/

/	1	1	\
\	0	1	/

x₁

M( le_in(x₁, x₂) ) =

/	0	\
\	0	/

/	1	1	\
\	1	1	/

x₁

/	1	0	\
\	0	0	/

x₂

M( .(x₁, x₂) ) =

/	1	\
\	0	/

/	1	0	\
\	1	0	/

x₁

/	1	0	\
\	0	1	/

x₂

M( gt_out ) =

/	0	\
\	1	/

M( gt_in(x₁, x₂) ) =

/	0	\
\	0	/

/	1	0	\
\	0	0	/

x₁

/	0	0	\
\	1	0	/

x₂

Tuple symbols:

M( U7¹(x₁, ..., x₅) ) =

[

]

x₁

[

]

x₂

[

]

x₃

[

]

x₄

[

]

x₅

M( U5¹(x₁, ..., x₅) ) =

[

]

x₁

[

]

x₂

[

]

x₃

[

]

x₄

[

]

x₅

M( MERGE_IN(x₁, x₂) ) =

[

]

x₁

[

]

x₂

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, s(Y)) → le_out
U10(gt_out) → gt_out
gt_in(s(X), 0) → gt_out
le_in(0, 0) → le_out
U11(le_out) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                        ↳ QDPOrderProof

                          ↳ QDP

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U7¹(A, X, B, Y, gt_in(A, B))
U5¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))

The TRS R consists of the following rules:

gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U10(gt_out) → gt_out
U11(le_out) → le_out

The set Q consists of the following terms:

gt_in(x0, x1)
le_in(x0, x1)
U10(x0)
U11(x0)

We have to consider all (P,Q,R)-chains.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SPLIT_IN(.(E, U), .(E, V), W) → SPLIT_IN(U, W, V)

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SPLIT_IN(.(E, U), .(E, V), W) → SPLIT_IN(U, W, V)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
SPLIT_IN(x1, x2, x3) = SPLIT_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SPLIT_IN(.(E, U)) → SPLIT_IN(U)

From the DPs we obtained the following set of size-change graphs:

SPLIT_IN(.(E, U)) → SPLIT_IN(U)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

MERGESORT_IN(.(E, .(F, U)), V) → U1¹(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → MERGESORT_IN(W, X)
U2¹(E, F, U, V, Y, mergesort_out(W, X)) → MERGESORT_IN(Y, Z)
U1¹(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2¹(E, F, U, V, Y, mergesort_in(W, X))

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U)), V) → U1(E, F, U, V, split_in(.(E, .(F, U)), W, Y))
split_in(.(E, U), .(E, V), W) → U9(E, U, V, W, split_in(U, W, V))
split_in([], [], []) → split_out([], [], [])
U9(E, U, V, W, split_out(U, W, V)) → split_out(.(E, U), .(E, V), W)
U1(E, F, U, V, split_out(.(E, .(F, U)), W, Y)) → U2(E, F, U, V, Y, mergesort_in(W, X))
mergesort_in(.(E, []), .(E, [])) → mergesort_out(.(E, []), .(E, []))
mergesort_in([], []) → mergesort_out([], [])
U2(E, F, U, V, Y, mergesort_out(W, X)) → U3(E, F, U, V, X, mergesort_in(Y, Z))
U3(E, F, U, V, X, mergesort_out(Y, Z)) → U4(E, F, U, V, merge_in(X, Z, V))
merge_in(.(A, X), .(B, Y), .(B, Z)) → U7(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), 0) → gt_out(s(X), 0)
gt_in(s(X), s(Y)) → U10(X, Y, gt_in(X, Y))
U10(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U7(A, X, B, Y, Z, gt_out(A, B)) → U8(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U5(A, X, B, Y, Z, le_in(A, B))
le_in(0, 0) → le_out(0, 0)
le_in(0, s(Y)) → le_out(0, s(Y))
le_in(s(X), s(Y)) → U11(X, Y, le_in(X, Y))
U11(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(A, X, B, Y, Z, le_out(A, B)) → U6(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U6(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U8(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))
U4(E, F, U, V, merge_out(X, Z, V)) → mergesort_out(.(E, .(F, U)), V)

The argument filtering Pi contains the following mapping:
mergesort_in(x1, x2) = mergesort_in(x1)
.(x1, x2) = .(x1, x2)
U1(x1, x2, x3, x4, x5) = U1(x5)
split_in(x1, x2, x3) = split_in(x1)
U9(x1, x2, x3, x4, x5) = U9(x1, x5)
[] = []
split_out(x1, x2, x3) = split_out(x2, x3)
U2(x1, x2, x3, x4, x5, x6) = U2(x5, x6)
mergesort_out(x1, x2) = mergesort_out(x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x5, x6)
U4(x1, x2, x3, x4, x5) = U4(x5)
merge_in(x1, x2, x3) = merge_in(x1, x2)
U7(x1, x2, x3, x4, x5, x6) = U7(x1, x2, x3, x4, x6)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
0 = 0
gt_out(x1, x2) = gt_out
U10(x1, x2, x3) = U10(x3)
U8(x1, x2, x3, x4, x5, x6) = U8(x3, x6)
U5(x1, x2, x3, x4, x5, x6) = U5(x1, x2, x3, x4, x6)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U11(x1, x2, x3) = U11(x3)
U6(x1, x2, x3, x4, x5, x6) = U6(x1, x6)
merge_out(x1, x2, x3) = merge_out(x3)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x5, x6)
U1¹(x1, x2, x3, x4, x5) = U1¹(x5)
MERGESORT_IN(x1, x2) = MERGESORT_IN(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U2¹(Y, mergesort_out(X)) → MERGESORT_IN(Y)
U1¹(split_out(W, Y)) → MERGESORT_IN(W)
MERGESORT_IN(.(E, .(F, U))) → U1¹(split_in(.(E, .(F, U))))
U1¹(split_out(W, Y)) → U2¹(Y, mergesort_in(W))

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U))) → U1(split_in(.(E, .(F, U))))
split_in(.(E, U)) → U9(E, split_in(U))
split_in([]) → split_out([], [])
U9(E, split_out(W, V)) → split_out(.(E, V), W)
U1(split_out(W, Y)) → U2(Y, mergesort_in(W))
mergesort_in(.(E, [])) → mergesort_out(.(E, []))
mergesort_in([]) → mergesort_out([])
U2(Y, mergesort_out(X)) → U3(X, mergesort_in(Y))
U3(X, mergesort_out(Z)) → U4(merge_in(X, Z))
merge_in(.(A, X), .(B, Y)) → U7(A, X, B, Y, gt_in(A, B))
gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
U7(A, X, B, Y, gt_out) → U8(B, merge_in(.(A, X), Y))
merge_in(.(A, X), .(B, Y)) → U5(A, X, B, Y, le_in(A, B))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out
U5(A, X, B, Y, le_out) → U6(A, merge_in(X, .(B, Y)))
merge_in([], X) → merge_out(X)
merge_in(X, []) → merge_out(X)
U6(A, merge_out(Z)) → merge_out(.(A, Z))
U8(B, merge_out(Z)) → merge_out(.(B, Z))
U4(merge_out(V)) → mergesort_out(V)

The set Q consists of the following terms:

mergesort_in(x0)
split_in(x0)
U9(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)
merge_in(x0, x1)
gt_in(x0, x1)
U10(x0)
U7(x0, x1, x2, x3, x4)
le_in(x0, x1)
U11(x0)
U5(x0, x1, x2, x3, x4)
U6(x0, x1)
U8(x0, x1)
U4(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule MERGESORT_IN(.(E, .(F, U))) → U1¹(split_in(.(E, .(F, U)))) at position [0] we obtained the following new rules:

MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, split_in(.(F, U))))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U1¹(split_out(W, Y)) → MERGESORT_IN(W)
U2¹(Y, mergesort_out(X)) → MERGESORT_IN(Y)
U1¹(split_out(W, Y)) → U2¹(Y, mergesort_in(W))
MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, split_in(.(F, U))))

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U))) → U1(split_in(.(E, .(F, U))))
split_in(.(E, U)) → U9(E, split_in(U))
split_in([]) → split_out([], [])
U9(E, split_out(W, V)) → split_out(.(E, V), W)
U1(split_out(W, Y)) → U2(Y, mergesort_in(W))
mergesort_in(.(E, [])) → mergesort_out(.(E, []))
mergesort_in([]) → mergesort_out([])
U2(Y, mergesort_out(X)) → U3(X, mergesort_in(Y))
U3(X, mergesort_out(Z)) → U4(merge_in(X, Z))
merge_in(.(A, X), .(B, Y)) → U7(A, X, B, Y, gt_in(A, B))
gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
U7(A, X, B, Y, gt_out) → U8(B, merge_in(.(A, X), Y))
merge_in(.(A, X), .(B, Y)) → U5(A, X, B, Y, le_in(A, B))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out
U5(A, X, B, Y, le_out) → U6(A, merge_in(X, .(B, Y)))
merge_in([], X) → merge_out(X)
merge_in(X, []) → merge_out(X)
U6(A, merge_out(Z)) → merge_out(.(A, Z))
U8(B, merge_out(Z)) → merge_out(.(B, Z))
U4(merge_out(V)) → mergesort_out(V)

The set Q consists of the following terms:

mergesort_in(x0)
split_in(x0)
U9(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)
merge_in(x0, x1)
gt_in(x0, x1)
U10(x0)
U7(x0, x1, x2, x3, x4)
le_in(x0, x1)
U11(x0)
U5(x0, x1, x2, x3, x4)
U6(x0, x1)
U8(x0, x1)
U4(x0)

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, split_in(.(F, U)))) at position [0,1] we obtained the following new rules:

MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, U9(F, split_in(U))))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U2¹(Y, mergesort_out(X)) → MERGESORT_IN(Y)
U1¹(split_out(W, Y)) → MERGESORT_IN(W)
MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, U9(F, split_in(U))))
U1¹(split_out(W, Y)) → U2¹(Y, mergesort_in(W))

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U))) → U1(split_in(.(E, .(F, U))))
split_in(.(E, U)) → U9(E, split_in(U))
split_in([]) → split_out([], [])
U9(E, split_out(W, V)) → split_out(.(E, V), W)
U1(split_out(W, Y)) → U2(Y, mergesort_in(W))
mergesort_in(.(E, [])) → mergesort_out(.(E, []))
mergesort_in([]) → mergesort_out([])
U2(Y, mergesort_out(X)) → U3(X, mergesort_in(Y))
U3(X, mergesort_out(Z)) → U4(merge_in(X, Z))
merge_in(.(A, X), .(B, Y)) → U7(A, X, B, Y, gt_in(A, B))
gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
U7(A, X, B, Y, gt_out) → U8(B, merge_in(.(A, X), Y))
merge_in(.(A, X), .(B, Y)) → U5(A, X, B, Y, le_in(A, B))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out
U5(A, X, B, Y, le_out) → U6(A, merge_in(X, .(B, Y)))
merge_in([], X) → merge_out(X)
merge_in(X, []) → merge_out(X)
U6(A, merge_out(Z)) → merge_out(.(A, Z))
U8(B, merge_out(Z)) → merge_out(.(B, Z))
U4(merge_out(V)) → mergesort_out(V)

The set Q consists of the following terms:

mergesort_in(x0)
split_in(x0)
U9(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)
merge_in(x0, x1)
gt_in(x0, x1)
U10(x0)
U7(x0, x1, x2, x3, x4)
le_in(x0, x1)
U11(x0)
U5(x0, x1, x2, x3, x4)
U6(x0, x1)
U8(x0, x1)
U4(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MERGESORT_IN(.(E, .(F, U))) → U1¹(U9(E, U9(F, split_in(U))))

The remaining pairs can at least be oriented weakly.

U2¹(Y, mergesort_out(X)) → MERGESORT_IN(Y)
U1¹(split_out(W, Y)) → MERGESORT_IN(W)
U1¹(split_out(W, Y)) → U2¹(Y, mergesort_in(W))

Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( [] ) =

/	0	\
\	0	/

M( U8(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( 0 ) =

/	0	\
\	0	/

M( U3(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( le_in(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( U5(x₁, ..., x₅) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

/	0	0	\
\	0	0	/

x₃

/	0	0	\
\	0	0	/

x₄

/	0	0	\
\	0	0	/

x₅

M( mergesort_in(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( U10(x₁) ) =

/	1	\
\	1	/

/	0	0	\
\	0	0	/

x₁

M( mergesort_out(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( s(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( U11(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( U7(x₁, ..., x₅) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

/	0	0	\
\	0	0	/

x₃

/	0	0	\
\	0	0	/

x₄

/	0	0	\
\	0	0	/

x₅

M( gt_in(x₁, x₂) ) =

/	1	\
\	1	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( le_out ) =

/	0	\
\	0	/

M( U6(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( split_in(x₁) ) =

/	0	\
\	1	/

/	1	1	\
\	0	1	/

x₁

M( U1(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( split_out(x₁, x₂) ) =

/	0	\
\	1	/

/	1	1	\
\	0	0	/

x₁

/	1	1	\
\	0	1	/

x₂

M( .(x₁, x₂) ) =

/	0	\
\	1	/

/	0	0	\
\	0	1	/

x₁

/	0	1	\
\	1	1	/

x₂

M( U2(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( gt_out ) =

/	0	\
\	0	/

M( merge_out(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( merge_in(x₁, x₂) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	0	\
\	0	0	/

x₂

M( U4(x₁) ) =

/	0	\
\	0	/

/	0	0	\
\	0	0	/

x₁

M( U9(x₁, x₂) ) =

/	0	\
\	1	/

/	0	1	\
\	0	1	/

x₁

/	1	1	\
\	1	0	/

x₂

Tuple symbols:

M( U1¹(x₁) ) =

[

]

x₁

M( MERGESORT_IN(x₁) ) =

[

]

x₁

M( U2¹(x₁, x₂) ) =

[

]

x₁

[

]

x₂

gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
split_in([]) → split_out([], [])
split_in(.(E, U)) → U9(E, split_in(U))
gt_in(s(X), 0) → gt_out
U9(E, split_out(W, V)) → split_out(.(E, V), W)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ PiDPToQDPProof

                  ↳ QDP

                    ↳ Rewriting

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U1¹(split_out(W, Y)) → MERGESORT_IN(W)
U2¹(Y, mergesort_out(X)) → MERGESORT_IN(Y)
U1¹(split_out(W, Y)) → U2¹(Y, mergesort_in(W))

The TRS R consists of the following rules:

mergesort_in(.(E, .(F, U))) → U1(split_in(.(E, .(F, U))))
split_in(.(E, U)) → U9(E, split_in(U))
split_in([]) → split_out([], [])
U9(E, split_out(W, V)) → split_out(.(E, V), W)
U1(split_out(W, Y)) → U2(Y, mergesort_in(W))
mergesort_in(.(E, [])) → mergesort_out(.(E, []))
mergesort_in([]) → mergesort_out([])
U2(Y, mergesort_out(X)) → U3(X, mergesort_in(Y))
U3(X, mergesort_out(Z)) → U4(merge_in(X, Z))
merge_in(.(A, X), .(B, Y)) → U7(A, X, B, Y, gt_in(A, B))
gt_in(s(X), 0) → gt_out
gt_in(s(X), s(Y)) → U10(gt_in(X, Y))
U10(gt_out) → gt_out
U7(A, X, B, Y, gt_out) → U8(B, merge_in(.(A, X), Y))
merge_in(.(A, X), .(B, Y)) → U5(A, X, B, Y, le_in(A, B))
le_in(0, 0) → le_out
le_in(0, s(Y)) → le_out
le_in(s(X), s(Y)) → U11(le_in(X, Y))
U11(le_out) → le_out
U5(A, X, B, Y, le_out) → U6(A, merge_in(X, .(B, Y)))
merge_in([], X) → merge_out(X)
merge_in(X, []) → merge_out(X)
U6(A, merge_out(Z)) → merge_out(.(A, Z))
U8(B, merge_out(Z)) → merge_out(.(B, Z))
U4(merge_out(V)) → mergesort_out(V)

The set Q consists of the following terms:

mergesort_in(x0)
split_in(x0)
U9(x0, x1)
U1(x0)
U2(x0, x1)
U3(x0, x1)
merge_in(x0, x1)
gt_in(x0, x1)
U10(x0)
U7(x0, x1, x2, x3, x4)
le_in(x0, x1)
U11(x0)
U5(x0, x1, x2, x3, x4)
U6(x0, x1)
U8(x0, x1)
U4(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.